INF551: Computational logic
from Artificial intelligence to Zero bugs
Samuel Mimram
´
Ecole Polytechnique
Let’s start with some polls
• English or French?
• Who has followed INF412?
• Who has already used OCaml?
• Who has already heard of a proof assistant?
1
Let’s start with some polls
• English or French?
• Who has followed INF412?
• Who has already used OCaml?
• Who has already heard of a proof assistant?
1
Let’s start with some polls
• English or French?
• Who has followed INF412?
• Who has already used OCaml?
• Who has already heard of a proof assistant?
1
Let’s start with some polls
• English or French?
• Who has followed INF412?
• Who has already used OCaml?
• Who has already heard of a proof assistant?
1
What is this course about?
PROGRAM
=
PROOF
2
What is this course about?
A rough history of the subject.
• 1900: formalization of the notion of proof
Hilbert, Frege, Russell, Brouwer, Gentzen, ...
• 1930: functional programming (λ-calculus)
Church, ...
• 1960: typing rules for functional programming = rules for logic
Curry, Howard, ...
• 1970: programs to verify proofs
de Bruijn, Coquand, ...
• 1970: dependent types
Martin-L¨of, Coquand, ...
3
What is this course about?
Γ ` f : A → A
(ax)
Γ ` f : A → A
(ax)
Γ ` x : A → A
(ax)
Γ ` fx : A
(→
E
)
f : A → A, x : A ` f (fx) : A
(→
E
)
f : A → A ` λx
A
.f (fx) : A → A
(→
I
)
` λf
A→A
.λx
A
.f (fx) : (A → A) → A → A
(→
I
)
4
What is this course about?
This correspondence between proofs and programs implies that
• we can automatically check whether a proof is valid or not,
• we can prove properties about programs,
• we can use programs to generate proofs.
5
Plan of the course
Programming proofs (TD in OCaml)
1. Typed functional programming
2. Intuitionistic propositional logic
3. λ-calculus
4. The proof-as-program correspondence
Proving programs (TD in Agda)
5. Introduction to Agda
6. First order logic
7. Dependent types I
8. Dependent types II
9. Homotopy type theory
6
Course notes
Samuel MIMRAM
8
Course notes
Samuel MIMRAM
8
Course notes
Samuel MIMRAM
8
Evaluation
You will be evaluated on
1. the TDs (33%),
2. an exam (33%),
3. the 4th TD/project with a presentation and course questions (33%).
Optionally, the default project can be replaced by a custom project or a presentation of
an article: in this case, contact me a few weeks in advance.
It is important that you submit your TD solutions on moodle.
(if you don’t have access to it, use mail)
10
Evaluation
Some general remarks:
• the goal is that you understand, please ask questions, including for the project,
• the subjects are long it is not necessary to finish them to have a good grade,
• do not forget to submit the PC on the moodle,
• the course focuses on theory and the PC focus on practice,
• it will be difficult for you to catch up, please attend courses.
11
Testing vs proving
Programming
Most programmers use tests in order to
validate their developments.
This is based on the belief that if the
program
• uses “regular enough” functions, and
• “small” constants,
then enough tests should cover all possible
behaviors.
Mathematics
No mathematician, in order to prove
∀n ∈ N.P(n)
will start checking P(0), then P(1), then
P(2), . . .
He will make a proof, which ensures that
P(n) holds whichever n ∈ N is.
Can we prove programs?
13
Testing vs proving
How much is
Z
∞
0
sin(t)
t
dt ?
14
Testing vs proving
15
Testing vs proving
Z
∞
0
sin(t)
t
dt =
π
2
Z
∞
0
sin(t)
t
sin(t/101)
t/101
dt =
π
2
Z
∞
0
sin(t)
t
sin(t/101)
t/101
sin(t/201)
t/201
dt =
π
2
Z
∞
0
sin(t)
t
sin(t/101)
t/101
sin(t/201)
t/201
sin(t/301)
t/301
dt =
π
2
.
.
.
Z
∞
0
n
Y
i =0
sin(t/(100i + 1))
t/(100i + 1)
!
dt =
16
Testing vs proving
Z
∞
0
sin(t)
t
dt =
π
2
Z
∞
0
sin(t)
t
sin(t/101)
t/101
dt =
π
2
Z
∞
0
sin(t)
t
sin(t/101)
t/101
sin(t/201)
t/201
dt =
π
2
Z
∞
0
sin(t)
t
sin(t/101)
t/101
sin(t/201)
t/201
sin(t/301)
t/301
dt =
π
2
.
.
.
Z
∞
0
n
Y
i =0
sin(t/(100i + 1))
t/(100i + 1)
!
dt =
16
Testing vs proving
Z
∞
0
sin(t)
t
dt =
π
2
Z
∞
0
sin(t)
t
sin(t/101)
t/101
dt =
π
2
Z
∞
0
sin(t)
t
sin(t/101)
t/101
sin(t/201)
t/201
dt =
π
2
Z
∞
0
sin(t)
t
sin(t/101)
t/101
sin(t/201)
t/201
sin(t/301)
t/301
dt =
π
2
.
.
.
Z
∞
0
n
Y
i =0
sin(t/(100i + 1))
t/(100i + 1)
!
dt =
16
Testing vs proving
Z
∞
0
sin(t)
t
dt =
π
2
Z
∞
0
sin(t)
t
sin(t/101)
t/101
dt =
π
2
Z
∞
0
sin(t)
t
sin(t/101)
t/101
sin(t/201)
t/201
dt =
π
2
Z
∞
0
sin(t)
t
sin(t/101)
t/101
sin(t/201)
t/201
sin(t/301)
t/301
dt =
π
2
.
.
.
Z
∞
0
n
Y
i =0
sin(t/(100i + 1))
t/(100i + 1)
!
dt =
16
Testing vs proving
Z
∞
0
sin(t)
t
dt =
π
2
Z
∞
0
sin(t)
t
sin(t/101)
t/101
dt =
π
2
Z
∞
0
sin(t)
t
sin(t/101)
t/101
sin(t/201)
t/201
dt =
π
2
Z
∞
0
sin(t)
t
sin(t/101)
t/101
sin(t/201)
t/201
sin(t/301)
t/301
dt =
π
2
.
.
.
Z
∞
0
n
Y
i =0
sin(t/(100i + 1))
t/(100i + 1)
!
dt =
16
Testing vs proving
Z
∞
0
sin(t)
t
dt =
π
2
Z
∞
0
sin(t)
t
sin(t/101)
t/101
dt =
π
2
Z
∞
0
sin(t)
t
sin(t/101)
t/101
sin(t/201)
t/201
dt =
π
2
Z
∞
0
sin(t)
t
sin(t/101)
t/101
sin(t/201)
t/201
sin(t/301)
t/301
dt =
π
2
.
.
.
Z
∞
0
n
Y
i =0
sin(t/(100i + 1))
t/(100i + 1)
!
dt =
16
Testing vs proving
Z
∞
0
sin(t)
t
dt =
π
2
Z
∞
0
sin(t)
t
sin(t/101)
t/101
dt =
π
2
Z
∞
0
sin(t)
t
sin(t/101)
t/101
sin(t/201)
t/201
dt =
π
2
Z
∞
0
sin(t)
t
sin(t/101)
t/101
sin(t/201)
t/201
sin(t/301)
t/301
dt =
π
2
.
.
.
Z
∞
0
n
Y
i =0
sin(t/(100i + 1))
t/(100i + 1)
!
dt =
16
Testing vs proving
Z
∞
0
sin(t)
t
dt =
π
2
Z
∞
0
sin(t)
t
sin(t/101)
t/101
dt =
π
2
Z
∞
0
sin(t)
t
sin(t/101)
t/101
sin(t/201)
t/201
dt =
π
2
Z
∞
0
sin(t)
t
sin(t/101)
t/101
sin(t/201)
t/201
sin(t/301)
t/301
dt =
π
2
.
.
.
Z
∞
0
n
Y
i =0
sin(t/(100i + 1))
t/(100i + 1)
!
dt =
16
Testing vs proving
In fact, the equality
Z
∞
0
n
Y
i =0
sin(t/(100n + 1))
t/(100n + 1)
!
dt =
π
2
starts breaking at
n = 15 341 178 777 673 149 429 167 740 440 969 249 338 310 889
17
The Therac-25
The Therac-25 was
• a radiation therapy machine with two modes:
low energy electrons (e.g. skin) and high energy X-rays (e.g. lungs),
• one day the operator pressed “x” instead of “e”, and quickly corrected to “e”
• the patient received 100 times the expected dose and eventually died
• there was a concurrency error: if an edit was performed during the magnet setting
phase (8 seconds) it was not taken into account because of the value of the
shared completion variable, although the screen made you think it did
• the bug was present in the Therac-20 but hardware prevented this
• there was an overflow in a 1 byte long variable which did also caused overdose
under bad cirumstances every 256 attempts
• first software bug to actually kill people
19
Ariane 5
Ariane 5
• reused the Ariane 5 reused the inertial reference platform
(SRI) from Ariane 4 (uses sensors to compute the position)
• the acceleration was 5 times bigger and converted from 64 bits to 16 bits, which
resulted in an overflow
• this caused a hardware exception, which caused sending test data on the data bus
• at t0+37, the autopilot is then launched, uses the test data as actual data, and
thus abruptly changes the trajectory of the rocket
• the SRI were useful only before launching and kept active during the 40 first
seconds because this was required by Ariane 4.
20
Proof assistants
Starting from the 70s, people started to develop proof assistants which are programs
which can check proofs (Agda, Coq, Isabelle, ...).
In such a program, you can
1. express logical formulas
2. gradually prove those formulas
3. extract a program from those proofs
Typical example:
∀l ∈ (List N).∃l
0
∈ (List N).(Sorted l
0
)
21
Proof assistants
Starting from the 70s, people started to develop proof assistants which are programs
which can check proofs (Agda, Coq, Isabelle, ...).
In such a program, you can
1. express logical formulas
2. gradually prove those formulas
3. extract a program from those proofs
Typical example:
∀l ∈ (List N).∃l
0
∈ (List N).(Sorted l
0
)
21
Proof assistants
22
Proof assistants
Those proof assistants guarantee that the program will always act according to the
specification...
...provided that you believe that those assistants do not have bugs:
• there is a deep well-established theory,
• most proof assistants have a small core,
• part of the proof assistants have been formalized using proof assistants.
PS: you also have to trust to compiler
• CompCert: a fully certified compiler
and the OS, and the hardware...
23
Proof assistants
Those proof assistants guarantee that the program will always act according to the
specification...
...provided that you believe that those assistants do not have bugs:
• there is a deep well-established theory,
• most proof assistants have a small core,
• part of the proof assistants have been formalized using proof assistants.
PS: you also have to trust to compiler
• CompCert: a fully certified compiler
and the OS, and the hardware...
23
Proof assistants
Those proof assistants guarantee that the program will always act according to the
specification...
...provided that you believe that those assistants do not have bugs:
• there is a deep well-established theory,
• most proof assistants have a small core,
• part of the proof assistants have been formalized using proof assistants.
PS: you also have to trust to compiler
• CompCert: a fully certified compiler
and the OS, and the hardware...
23
Formal methods
Proof assistants are part of formal methods, which guarantee behavior of programs.
24
Formal methods
Proof assistants are part of formal methods, which guarantee behavior of programs.
There are various level of automation:
• fully automatic (abstract interpretation, etc.),
• partially automated (Hoare logic, etc.)
• manual (proof assistants, etc.)
In general, more automated means faster but more specific.
24
Formal methods
Proof assistants are part of formal methods, which guarantee behavior of programs.
They have been successfully used in industry:
• line 14 and Roissy Val (B-method)
• Airbus
• ...
It takes lots of time (money), but achieves high level of guarantee.
RATP / CML / Agence Cartographique / PLM 9.2012 - B BO
Cour Saint-Émilion
Bercy
Gare de Lyon
Châtelet
Pyramides
Madeleine
Saint-Lazare
Bibliothèque
François Mitterrand
Olympiades
Gare de Paris–Bercy
Orly
CDG
24
Formal methods
Proof assistants are part of formal methods, which guarantee behavior of programs.
They have been successfully used in industry:
• line 14 and Roissy Val (B-method)
• Airbus
• ...
It takes lots of time (money), but achieves high level of guarantee.
RATP / CML / Agence Cartographique / PLM 9.2012 - B BO
Cour Saint-Émilion
Bercy
Gare de Lyon
Châtelet
Pyramides
Madeleine
Saint-Lazare
Bibliothèque
François Mitterrand
Olympiades
Gare de Paris–Bercy
Orly
CDG
24
Formal methods
Proof assistants are part of formal methods, which guarantee behavior of programs.
They have been successfully used in industry:
• line 14 and Roissy Val (B-method)
• Airbus
• ...
It takes lots of time (money), but achieves high level of guarantee.
RATP / CML / Agence Cartographique / PLM 9.2012 - B BO
Cour Saint-Émilion
Bercy
Gare de Lyon
Châtelet
Pyramides
Madeleine
Saint-Lazare
Bibliothèque
François Mitterrand
Olympiades
Gare de Paris–Bercy
Orly
CDG
24
In this course
The most complicated algorithm that you will prove here is a sorting algorithm.
I can hear you think: “come on, in 2021, we know how to implement sorting”, but
• proving more complex programs is “only” a matter of time,
• in 2015, a bug was found in the default implementation of sorting in Java.
26
In this course
The most complicated algorithm that you will prove here is a sorting algorithm.
I can hear you think: “come on, in 2021, we know how to implement sorting”, but
• proving more complex programs is “only” a matter of time,
• in 2015, a bug was found in the default implementation of sorting in Java.
26
In this course
The most complicated algorithm that you will prove here is a sorting algorithm.
I can hear you think: “come on, in 2021, we know how to implement sorting”, but
• proving more complex programs is “only” a matter of time,
• in 2015, a bug was found in the default implementation of sorting in Java.
26
In this course
The most complicated algorithm that you will prove here is a sorting algorithm.
I can hear you think: “come on, in 2021, we know how to implement sorting”, but
• proving more complex programs is “only” a matter of time,
• in 2015, a bug was found in the default implementation of sorting in Java.
26
Proof checking
Mathematicians are humans and they happen to make mistakes.
For instance,
• 1991: the Fields medalist Voevodsky solves a conjecture of Grothendieck,
“spaces = strict ∞-categories with weakly invertible morphisms”
• 1998: Simpson finds a counter-example
• 2005: Voevodsky gets interested in proof assistants
• 2010: Voevodsky develop new foundations for mathematics
homotopy type theory
• 2013: Voevodsky finally accepts that there is a flaw in his proof
27
Proof checking
Mathematicians are humans and they happen to make mistakes.
For instance,
• 1991: the Fields medalist Voevodsky solves a conjecture of Grothendieck,
“spaces = strict ∞-categories with weakly invertible morphisms”
• 1998: Simpson finds a counter-example
• 2005: Voevodsky gets interested in proof assistants
• 2010: Voevodsky develop new foundations for mathematics
homotopy type theory
• 2013: Voevodsky finally accepts that there is a flaw in his proof
27
Proof checking
Mathematicians are humans and they happen to make mistakes.
For instance,
• 1991: the Fields medalist Voevodsky solves a conjecture of Grothendieck,
“spaces = strict ∞-categories with weakly invertible morphisms”
• 1998: Simpson finds a counter-example
• 2005: Voevodsky gets interested in proof assistants
• 2010: Voevodsky develop new foundations for mathematics
homotopy type theory
• 2013: Voevodsky finally accepts that there is a flaw in his proof
27
Proof checking
Mathematicians are humans and they happen to make mistakes.
For instance,
• 1991: the Fields medalist Voevodsky solves a conjecture of Grothendieck,
“spaces = strict ∞-categories with weakly invertible morphisms”
• 1998: Simpson finds a counter-example
• 2005: Voevodsky gets interested in proof assistants
• 2010: Voevodsky develop new foundations for mathematics
homotopy type theory
• 2013: Voevodsky finally accepts that there is a flaw in his proof
27
Proof checking
Mathematicians are humans and they happen to make mistakes.
For instance,
• 1991: the Fields medalist Voevodsky solves a conjecture of Grothendieck,
“spaces = strict ∞-categories with weakly invertible morphisms”
• 1998: Simpson finds a counter-example
• 2005: Voevodsky gets interested in proof assistants
• 2010: Voevodsky develop new foundations for mathematics
homotopy type theory
• 2013: Voevodsky finally accepts that there is a flaw in his proof
27
Proof checking
Quoting Voevodsky:
In the Spring of 2010 I suggested to the School of Mathematics that I will
organize a special program on new foundations of mathematics in 2012/13,
despite the fact that at this time it was not clear that the field would be
ready for such a program by then.
I now do my mathematics with a proof assistant and do not have to worry
all the time about mistakes in my arguments or about how to convince
others that my arguments are correct.
But I think that the sense of urgency that pushed me to hurry with the
program remains. Sooner or later computer proof assistants will become
the norm, but the longer this process takes the more misery associated
with mistakes and with unnecessary self-verification the practitioners of the
field will have to endure.
�28
28
Proof checking
Quoting Voevodsky:
In the Spring of 2010 I suggested to the School of Mathematics that I will
organize a special program on new foundations of mathematics in 2012/13,
despite the fact that at this time it was not clear that the field would be
ready for such a program by then.
I now do my mathematics with a proof assistant and do not have to worry
all the time about mistakes in my arguments or about how to convince
others that my arguments are correct.
But I think that the sense of urgency that pushed me to hurry with the
program remains. Sooner or later computer proof assistants will become
the norm, but the longer this process takes the more misery associated
with mistakes and with unnecessary self-verification the practitioners of the
field will have to endure.
�28
28
Proof checking
Quoting Voevodsky:
In the Spring of 2010 I suggested to the School of Mathematics that I will
organize a special program on new foundations of mathematics in 2012/13,
despite the fact that at this time it was not clear that the field would be
ready for such a program by then.
I now do my mathematics with a proof assistant and do not have to worry
all the time about mistakes in my arguments or about how to convince
others that my arguments are correct.
But I think that the sense of urgency that pushed me to hurry with the
program remains. Sooner or later computer proof assistants will become
the norm, but the longer this process takes the more misery associated
with mistakes and with unnecessary self-verification the practitioners of the
field will have to endure.
�28
28
Proof checking
Nowadays, in addition to applied mathematics, important mathematical theorems have
been formalized:
• the four color theorem (graph theory)
• the Feit-Thompson theorem (group theory)
29
Types as foundations
What is mathematics talking about?
• 1901: Russell’s paradox in naive set theory
• 1908: Zermelo-Fraenkel set theory
• 1912: Russell’s theory of types
• 2013: Voevodsky’s homotopy type theory: type = space
30
Proof searching
Understanding proof theory allows to
• formulate problems in a logical fashion,
• design new proof search procedures.
In fact, McCarthy, one of the founder of Artificial Intelligence, was an advocate of
using computational logic in order to represent knowledge and manipulate data.
[Admittedly this is less popular than neural networks today, but one never knows]
We don’t insist on this here, because these procedures give you little control about the
proofs they produce.
31
Proof searching
Understanding proof theory allows to
• formulate problems in a logical fashion,
• design new proof search procedures.
In fact, McCarthy, one of the founder of Artificial Intelligence, was an advocate of
using computational logic in order to represent knowledge and manipulate data.
[Admittedly this is less popular than neural networks today, but one never knows]
We don’t insist on this here, because these procedures give you little control about the
proofs they produce.
31
Philosophy
This also provides answer to philosophical / epistemological questions:
• what are the foundations of mathematics?
• what is reasoning?
• what is a proof?
• what does it mean that something exists?
• what does it mean for two things to be equal?
• . . .
32
Religion
Some people base their faith on the computational trinitarism:
CategoriesProgramming
Logic
33
Religion
Some people base their faith on the computational trinitarism:
CategoriesProgramming
Logic
33
Religion
Some people base their faith on the computational trinitarism:
CategoriesProgramming
Logic
33
OCaml in three slides
let x = 5
let f x = 2 * x
let () =
print_string "The result is ";
print_int (f 5)
let rec fact n =
if n = 0 then 1 else n * (fact (n-1))
35
OCaml in three slides
let x = 5
let f x = 2 * x
let () =
print_string "The result is ";
print_int (f 5)
let rec fact n =
if n = 0 then 1 else n * (fact (n-1))
35
OCaml in three slides
let x = 5
let f x = 2 * x
let () =
print_string "The result is ";
print_int (f 5)
let rec fact n =
if n = 0 then 1 else n * (fact (n-1))
35
OCaml in three slides
let x = 5
let f x = 2 * x
let () =
print_string "The result is ";
print_int (f 5)
let rec fact n =
if n = 0 then 1 else n * (fact (n-1))
35
OCaml in three slides
let rec map f l =
match l with
| [] -> []
| x::l -> (f x)::(map f l)
let () =
let l1 = [1;2;3] in
let l2 = map (fun x -> 2*x) l1 in
assert (l1 = l2)
36
OCaml in three slides
let rec map f l =
match l with
| [] -> []
| x::l -> (f x)::(map f l)
let () =
let l1 = [1;2;3] in
let l2 = map (fun x -> 2*x) l1 in
assert (l1 = l2)
36
OCaml in three slides
• comparison: = and <> (never == nor !=)
• boolean operations: &&, ||, not
• string concatenation: s ^ t
• patterns always bind:
• beware of imbricated patterns
37
OCaml in three slides
• comparison: = and <> (never == nor !=)
• boolean operations: &&, ||, not
• string concatenation: s ^ t
• patterns always bind:
• beware of imbricated patterns
37
OCaml in three slides
• comparison: = and <> (never == nor !=)
• boolean operations: &&, ||, not
• string concatenation: s ^ t
• patterns always bind:
• beware of imbricated patterns
37
OCaml in three slides
• comparison: = and <> (never == nor !=)
• boolean operations: &&, ||, not
• string concatenation: s ^ t
• patterns always bind:
let is_singleton n l =
match l with
| [n] -> true
| _ -> false
is not what you think
• beware of imbricated patterns
37
OCaml in three slides
• comparison: = and <> (never == nor !=)
• boolean operations: &&, ||, not
• string concatenation: s ^ t
• patterns always bind:
let is_singleton n l =
match l with
| [m] when m = n -> true
| _ -> false
is how you should write it
• beware of imbricated patterns
37
OCaml in three slides
• comparison: = and <> (never == nor !=)
• boolean operations: &&, ||, not
• string concatenation: s ^ t
• patterns always bind:
• beware of imbricated patterns
let is_singleton_singleton l =
match l with
| [l'] ->
match l' with
| [l''] -> true
| _ -> false
| _ -> false
is not what your think
37
OCaml in three slides
• comparison: = and <> (never == nor !=)
• boolean operations: &&, ||, not
• string concatenation: s ^ t
• patterns always bind:
• beware of imbricated patterns
let is_singleton_singleton l =
match l with
| [l'] ->
match l' with
| [l''] -> true
| _ -> false
| _ -> false
is how OCaml reads it
37
OCaml in three slides
• comparison: = and <> (never == nor !=)
• boolean operations: &&, ||, not
• string concatenation: s ^ t
• patterns always bind:
• beware of imbricated patterns
let is_singleton_singleton l =
match l with
| [l'] -> (
match l' with
| [l''] -> true
| _ -> false
)
| _ -> false
is how you should write it
37
Types in OCaml
Every program has a type:
expression type
3
int
3.0 float
true bool
() unit
fun x -> 2 * x int -> int
fun x -> (2 * x, "x") int -> int * string
fun x -> (x, "x") ’a -> ’a * string
[3; 4; 1] int list
[] ’a list
List.map ’a list -> (’a -> ’b) -> ’b list
print string string -> unit
fun x -> x x Error: This expression has type ’a -> ’b but an expression was expected of type ’a The type variable ’a occurs inside ’a -> ’b
38
Types in OCaml
Every program has a type:
expression type
3 int
3.0 float
true bool
() unit
fun x -> 2 * x int -> int
fun x -> (2 * x, "x") int -> int * string
fun x -> (x, "x") ’a -> ’a * string
[3; 4; 1] int list
[] ’a list
List.map ’a list -> (’a -> ’b) -> ’b list
print string string -> unit
fun x -> x x Error: This expression has type ’a -> ’b but an expression was expected of type ’a The type variable ’a occurs inside ’a -> ’b
38
Types in OCaml
Every program has a type:
expression type
3 int
3.0
float
true bool
() unit
fun x -> 2 * x int -> int
fun x -> (2 * x, "x") int -> int * string
fun x -> (x, "x") ’a -> ’a * string
[3; 4; 1] int list
[] ’a list
List.map ’a list -> (’a -> ’b) -> ’b list
print string string -> unit
fun x -> x x Error: This expression has type ’a -> ’b but an expression was expected of type ’a The type variable ’a occurs inside ’a -> ’b
38
Types in OCaml
Every program has a type:
expression type
3 int
3.0 float
true bool
() unit
fun x -> 2 * x int -> int
fun x -> (2 * x, "x") int -> int * string
fun x -> (x, "x") ’a -> ’a * string
[3; 4; 1] int list
[] ’a list
List.map ’a list -> (’a -> ’b) -> ’b list
print string string -> unit
fun x -> x x Error: This expression has type ’a -> ’b but an expression was expected of type ’a The type variable ’a occurs inside ’a -> ’b
38
Types in OCaml
Every program has a type:
expression type
3 int
3.0 float
true
bool
() unit
fun x -> 2 * x int -> int
fun x -> (2 * x, "x") int -> int * string
fun x -> (x, "x") ’a -> ’a * string
[3; 4; 1] int list
[] ’a list
List.map ’a list -> (’a -> ’b) -> ’b list
print string string -> unit
fun x -> x x Error: This expression has type ’a -> ’b but an expression was expected of type ’a The type variable ’a occurs inside ’a -> ’b
38
Types in OCaml
Every program has a type:
expression type
3 int
3.0 float
true bool
() unit
fun x -> 2 * x int -> int
fun x -> (2 * x, "x") int -> int * string
fun x -> (x, "x") ’a -> ’a * string
[3; 4; 1] int list
[] ’a list
List.map ’a list -> (’a -> ’b) -> ’b list
print string string -> unit
fun x -> x x Error: This expression has type ’a -> ’b but an expression was expected of type ’a The type variable ’a occurs inside ’a -> ’b
38
Types in OCaml
Every program has a type:
expression type
3 int
3.0 float
true bool
()
unit
fun x -> 2 * x int -> int
fun x -> (2 * x, "x") int -> int * string
fun x -> (x, "x") ’a -> ’a * string
[3; 4; 1] int list
[] ’a list
List.map ’a list -> (’a -> ’b) -> ’b list
print string string -> unit
fun x -> x x Error: This expression has type ’a -> ’b but an expression was expected of type ’a The type variable ’a occurs inside ’a -> ’b
38
Types in OCaml
Every program has a type:
expression type
3 int
3.0 float
true bool
() unit
fun x -> 2 * x int -> int
fun x -> (2 * x, "x") int -> int * string
fun x -> (x, "x") ’a -> ’a * string
[3; 4; 1] int list
[] ’a list
List.map ’a list -> (’a -> ’b) -> ’b list
print string string -> unit
fun x -> x x Error: This expression has type ’a -> ’b but an expression was expected of type ’a The type variable ’a occurs inside ’a -> ’b
38
Types in OCaml
Every program has a type:
expression type
3 int
3.0 float
true bool
() unit
fun x -> 2 * x
int -> int
fun x -> (2 * x, "x") int -> int * string
fun x -> (x, "x") ’a -> ’a * string
[3; 4; 1] int list
[] ’a list
List.map ’a list -> (’a -> ’b) -> ’b list
print string string -> unit
fun x -> x x Error: This expression has type ’a -> ’b but an expression was expected of type ’a The type variable ’a occurs inside ’a -> ’b
38
Types in OCaml
Every program has a type:
expression type
3 int
3.0 float
true bool
() unit
fun x -> 2 * x int -> int
fun x -> (2 * x, "x") int -> int * string
fun x -> (x, "x") ’a -> ’a * string
[3; 4; 1] int list
[] ’a list
List.map ’a list -> (’a -> ’b) -> ’b list
print string string -> unit
fun x -> x x Error: This expression has type ’a -> ’b but an expression was expected of type ’a The type variable ’a occurs inside ’a -> ’b
38
Types in OCaml
Every program has a type:
expression type
3 int
3.0 float
true bool
() unit
fun x -> 2 * x int -> int
fun x -> (2 * x, "x")
int -> int * string
fun x -> (x, "x") ’a -> ’a * string
[3; 4; 1] int list
[] ’a list
List.map ’a list -> (’a -> ’b) -> ’b list
print string string -> unit
fun x -> x x Error: This expression has type ’a -> ’b but an expression was expected of type ’a The type variable ’a occurs inside ’a -> ’b
38
Types in OCaml
Every program has a type:
expression type
3 int
3.0 float
true bool
() unit
fun x -> 2 * x int -> int
fun x -> (2 * x, "x") int -> int * string
fun x -> (x, "x") ’a -> ’a * string
[3; 4; 1] int list
[] ’a list
List.map ’a list -> (’a -> ’b) -> ’b list
print string string -> unit
fun x -> x x Error: This expression has type ’a -> ’b but an expression was expected of type ’a The type variable ’a occurs inside ’a -> ’b
38
Types in OCaml
Every program has a type:
expression type
3 int
3.0 float
true bool
() unit
fun x -> 2 * x int -> int
fun x -> (2 * x, "x") int -> int * string
fun x -> (x, "x")
’a -> ’a * string
[3; 4; 1] int list
[] ’a list
List.map ’a list -> (’a -> ’b) -> ’b list
print string string -> unit
fun x -> x x Error: This expression has type ’a -> ’b but an expression was expected of type ’a The type variable ’a occurs inside ’a -> ’b
38
Types in OCaml
Every program has a type:
expression type
3 int
3.0 float
true bool
() unit
fun x -> 2 * x int -> int
fun x -> (2 * x, "x") int -> int * string
fun x -> (x, "x") ’a -> ’a * string
[3; 4; 1] int list
[] ’a list
List.map ’a list -> (’a -> ’b) -> ’b list
print string string -> unit
fun x -> x x Error: This expression has type ’a -> ’b but an expression was expected of type ’a The type variable ’a occurs inside ’a -> ’b
38
Types in OCaml
Every program has a type:
expression type
3 int
3.0 float
true bool
() unit
fun x -> 2 * x int -> int
fun x -> (2 * x, "x") int -> int * string
fun x -> (x, "x") ’a -> ’a * string
[3; 4; 1]
int list
[] ’a list
List.map ’a list -> (’a -> ’b) -> ’b list
print string string -> unit
fun x -> x x Error: This expression has type ’a -> ’b but an expression was expected of type ’a The type variable ’a occurs inside ’a -> ’b
38
Types in OCaml
Every program has a type:
expression type
3 int
3.0 float
true bool
() unit
fun x -> 2 * x int -> int
fun x -> (2 * x, "x") int -> int * string
fun x -> (x, "x") ’a -> ’a * string
[3; 4; 1] int list
[] ’a list
List.map ’a list -> (’a -> ’b) -> ’b list
print string string -> unit
fun x -> x x Error: This expression has type ’a -> ’b but an expression was expected of type ’a The type variable ’a occurs inside ’a -> ’b
38
Types in OCaml
Every program has a type:
expression type
3 int
3.0 float
true bool
() unit
fun x -> 2 * x int -> int
fun x -> (2 * x, "x") int -> int * string
fun x -> (x, "x") ’a -> ’a * string
[3; 4; 1] int list
[]
’a list
List.map ’a list -> (’a -> ’b) -> ’b list
print string string -> unit
fun x -> x x Error: This expression has type ’a -> ’b but an expression was expected of type ’a The type variable ’a occurs inside ’a -> ’b
38
Types in OCaml
Every program has a type:
expression type
3 int
3.0 float
true bool
() unit
fun x -> 2 * x int -> int
fun x -> (2 * x, "x") int -> int * string
fun x -> (x, "x") ’a -> ’a * string
[3; 4; 1] int list
[] ’a list
List.map ’a list -> (’a -> ’b) -> ’b list
print string string -> unit
fun x -> x x Error: This expression has type ’a -> ’b but an expression was expected of type ’a The type variable ’a occurs inside ’a -> ’b
38
Types in OCaml
Every program has a type:
expression type
3 int
3.0 float
true bool
() unit
fun x -> 2 * x int -> int
fun x -> (2 * x, "x") int -> int * string
fun x -> (x, "x") ’a -> ’a * string
[3; 4; 1] int list
[] ’a list
List.map
’a list -> (’a -> ’b) -> ’b list
print string string -> unit
fun x -> x x Error: This expression has type ’a -> ’b but an expression was expected of type ’a The type variable ’a occurs inside ’a -> ’b
38
Types in OCaml
Every program has a type:
expression type
3 int
3.0 float
true bool
() unit
fun x -> 2 * x int -> int
fun x -> (2 * x, "x") int -> int * string
fun x -> (x, "x") ’a -> ’a * string
[3; 4; 1] int list
[] ’a list
List.map ’a list -> (’a -> ’b) -> ’b list
print string string -> unit
fun x -> x x Error: This expression has type ’a -> ’b but an expression was expected of type ’a The type variable ’a occurs inside ’a -> ’b
38
Types in OCaml
Every program has a type:
expression type
3 int
3.0 float
true bool
() unit
fun x -> 2 * x int -> int
fun x -> (2 * x, "x") int -> int * string
fun x -> (x, "x") ’a -> ’a * string
[3; 4; 1] int list
[] ’a list
List.map ’a list -> (’a -> ’b) -> ’b list
print string
string -> unit
fun x -> x x Error: This expression has type ’a -> ’b but an expression was expected of type ’a The type variable ’a occurs inside ’a -> ’b
38
Types in OCaml
Every program has a type:
expression type
3 int
3.0 float
true bool
() unit
fun x -> 2 * x int -> int
fun x -> (2 * x, "x") int -> int * string
fun x -> (x, "x") ’a -> ’a * string
[3; 4; 1] int list
[] ’a list
List.map ’a list -> (’a -> ’b) -> ’b list
print string string -> unit
fun x -> x x Error: This expression has type ’a -> ’b but an expression was expected of type ’a The type variable ’a occurs inside ’a -> ’b
38
Types in OCaml
Every program has a type:
expression type
3 int
3.0 float
true bool
() unit
fun x -> 2 * x int -> int
fun x -> (2 * x, "x") int -> int * string
fun x -> (x, "x") ’a -> ’a * string
[3; 4; 1] int list
[] ’a list
List.map ’a list -> (’a -> ’b) -> ’b list
print string string -> unit
fun x -> x x
Error: This expression has type ’a -> ’b but an expression was expected of type ’a The type variable ’a occurs inside ’a -> ’b
38
Types in OCaml
Every program has a type:
expression type
3 int
3.0 float
true bool
() unit
fun x -> 2 * x int -> int
fun x -> (2 * x, "x") int -> int * string
fun x -> (x, "x") ’a -> ’a * string
[3; 4; 1] int list
[] ’a list
List.map ’a list -> (’a -> ’b) -> ’b list
print string string -> unit
fun x -> x x Error: This expression has type ’a -> ’b but an expression was expected of type ’a The type variable ’a occurs inside ’a -> ’b
38
Types in OCaml
Typing guarantees that functions will always get arguments as expected.
The following will be rejected:
3 * "x"
a.(2.1)
.
.
.
but also
"abc" ^ 3
4 + 2.1
.
.
.
More on this later.
39
Types in OCaml
Typing guarantees that functions will always get arguments as expected.
The following will be rejected:
3 * "x"
a.(2.1)
.
.
.
but also
"abc" ^ 3
4 + 2.1
.
.
.
More on this later.
39
Types in OCaml
Types in OCaml are
• static: checked at compilation time,
• inferred: no type annotation is required, the compiler “guesses” the type,
• polymorphic: a type such as
’a -> ’a
is implicitly universally quantified on ’a,
• principal: the most general type is always inferred
fun x -> x : 'a -> 'a
but we can specify types if we want
fun (x : int) -> x : int -> int
40
Types in OCaml
Types in OCaml are
• static: checked at compilation time,
• inferred: no type annotation is required, the compiler “guesses” the type,
• polymorphic: a type such as
’a -> ’a
is implicitly universally quantified on ’a,
• principal: the most general type is always inferred
fun x -> x : 'a -> 'a
but we can specify types if we want
fun (x : int) -> x : int -> int
40
Types in OCaml
Types in OCaml are
• static: checked at compilation time,
• inferred: no type annotation is required, the compiler “guesses” the type,
• polymorphic: a type such as
’a -> ’a
is implicitly universally quantified on ’a,
• principal: the most general type is always inferred
fun x -> x : 'a -> 'a
but we can specify types if we want
fun (x : int) -> x : int -> int
40
Types in OCaml
Types in OCaml are
• static: checked at compilation time,
• inferred: no type annotation is required, the compiler “guesses” the type,
• polymorphic: a type such as
’a -> ’a
is implicitly universally quantified on ’a,
• principal: the most general type is always inferred
fun x -> x : 'a -> 'a
but we can specify types if we want
fun (x : int) -> x : int -> int
40
Types in OCaml
Types in OCaml are
• static: checked at compilation time,
• inferred: no type annotation is required, the compiler “guesses” the type,
• polymorphic: a type such as
’a -> ’a
is implicitly universally quantified on ’a,
• principal: the most general type is always inferred
fun x -> x : 'a -> 'a
but we can specify types if we want
fun (x : int) -> x : int -> int
40
Recursive types
Values of recursive types can be observed by pattern matching.
For instance, on lists:
let rec length l =
match l with
| [] -> 0
| x::l -> 1 + length l
41
Recursive types
We can also define custom recursive types:
type ilist =
| Nil
| Cons of int * ilist
A typical value is
Nil
Cons (3 , Nil)
Cons (5 , Cons (3 , Nil))
.
.
.
42
Recursive types
We can also define custom recursive types:
type ilist =
| Nil
| Cons of int * ilist
A typical value is
Nil
Cons (3 , Nil)
Cons (5 , Cons (3 , Nil))
.
.
.
42
Recursive types
We can also define custom recursive types:
type ilist =
| Nil
| Cons of int * ilist
A typical value is
Nil
Cons (3 , Nil)
Cons (5 , Cons (3 , Nil))
.
.
.
42
Recursive types
We can also define custom recursive types:
type ilist =
| Nil
| Cons of int * ilist
A typical value is
Nil
Cons (3 , Nil)
Cons (5 , Cons (3 , Nil))
.
.
.
42
Recursive types
We can also define custom recursive types:
type ilist =
| Nil
| Cons of int * ilist
A typical value is
Nil
Cons (3 , Nil)
Cons (5 , Cons (3 , Nil))
.
.
.
42
Recursive types
We can also define custom parametrized recursive types:
type 'a list =
| Nil
| Cons of 'a * 'a list
A typical value is
Nil
Cons (3 , Nil)
Cons (5 , Cons (3 , Nil))
.
.
.
42
Recursive types
We can also define custom parametrized recursive types:
type 'a list =
| []
| 'a :: 'a list
A typical value is
Nil
Cons (3 , Nil)
Cons (5 , Cons (3 , Nil))
.
.
.
42
Recursive types
Functions on recursive types are typically defined by recurrence:
let rec length l =
match l with
| Nil -> 0
| Cons (x , l') -> 1 + length l'
43
Recursive types
Functions on recursive types are typically defined by recurrence:
let rec concat l m =
match l with
| Nil -> m
| Cons (x , l') -> Cons (x , concat l' m)
43
Recursive types
Many usual types can be defined as recursive types.
Booleans:
type bool =
| True
| False
Conditional if b then e1 else e2 can be written as
44
Recursive types
Many usual types can be defined as recursive types.
Booleans:
type bool =
| True
| False
Conditional if b then e1 else e2 can be written as
44
Recursive types
Many usual types can be defined as recursive types.
Booleans:
type bool =
| True
| False
Conditional if b then e1 else e2 can be written as
match b with
| True -> e1
| False -> e2
44
Recursive types
Many usual types can be defined as recursive types.
Natural numbers (in unary notation):
type nat =
| Z
| S of nat
Addition can be computed as
let rec add x y =
match x with
| Z -> y
| S x' -> S (add x' y)
44
Recursive types
Many usual types can be defined as recursive types.
Natural numbers (in unary notation):
type nat =
| Z
| S of nat
Addition can be computed as
let rec add x y =
match x with
| Z -> y
| S x' -> S (add x' y)
44
Recursive types
Many usual types can be defined as recursive types.
Natural numbers (in unary notation):
type nat =
| Z
| S of nat
Addition can be computed as
let rec add x y =
match x with
| Z -> y
| S x' -> S (add x' y)
44
Recursive types
Many usual types can be defined as recursive types.
Unit:
type unit =
| T
which is usually written () instead of T.
A function let f () = e can be written as
44
Recursive types
Many usual types can be defined as recursive types.
Unit:
type unit =
| T
which is usually written () instead of T.
A function let f () = e can be written as
44
Recursive types
Many usual types can be defined as recursive types.
Unit:
type unit =
| T
which is usually written () instead of T.
A function let f () = e can be written as
let f x =
match x with
| T -> e
44
Other types
There are other ways of building types:
• products:
(3 , "x") is of type int * string
• records, objects, etc.
45
Other types
There are other ways of building types:
• products:
(3 , "x") is of type int * string
• records, objects, etc.
45
Types as formulas
There is a wonderful thing, called the proof-as-program correspondence, due to
and
Curry Howard
which states that
a type is the same as a formula
and
a program is the same as a proof.
47
Arrow as implication
Given types T and U, the type
T -> U
• the type of functions from T to U,
• the type of programs which transform a T into a U,
• the type of programs thanks to which having a T implies having a U,
• the formula T ⇒ U,
• the type of proofs of T ⇒ U.
Think of string of int of type int -> string.
48
Arrow as implication
Given types T and U, the type
T -> U
• the type of functions from T to U,
• the type of programs which transform a T into a U,
• the type of programs thanks to which having a T implies having a U,
• the formula T ⇒ U,
• the type of proofs of T ⇒ U.
Think of string of int of type int -> string.
48
Arrow as implication
Given types T and U, the type
T -> U
• the type of functions from T to U,
• the type of programs which transform a T into a U,
• the type of programs thanks to which having a T implies having a U,
• the formula T ⇒ U,
• the type of proofs of T ⇒ U.
Think of string of int of type int -> string.
48
Arrow as implication
Given types T and U, the type
T -> U
• the type of functions from T to U,
• the type of programs which transform a T into a U,
• the type of programs thanks to which having a T implies having a U,
• the formula T ⇒ U,
• the type of proofs of T ⇒ U.
Think of string of int of type int -> string.
48
Arrow as implication
Given types T and U, the type
T -> U
• the type of functions from T to U,
• the type of programs which transform a T into a U,
• the type of programs thanks to which having a T implies having a U,
• the formula T ⇒ U,
• the type of proofs of T ⇒ U.
Think of string of int of type int -> string.
48
Arrow as implication
We can thus think of a program of type
’a -> ’a
as a proof of
A ⇒ A
It can be proved by
let id = fun x -> x
49
Arrow as implication
We can thus think of a program of type
’a -> ’a
as a proof of
A ⇒ A
It can be proved by
let id = fun x -> x
49
Arrow as implication
We can thus think of a program of type
’a -> ’a
as a proof of
A ⇒ A
It can be proved by
let id = fun x -> x
49
Arrow as implication
The formula
A ⇒ B ⇒ A
i.e. the type
’a -> ’b -> ’a
can be proved by
let k = fun x y -> x
50
Arrow as implication
The formula
A ⇒ B ⇒ A
i.e. the type
’a -> ’b -> ’a
can be proved by
let k = fun x y -> x
50
Arrow as implication
The formula
A ⇒ B ⇒ A
i.e. the type
’a -> ’b -> ’a
can be proved by
let k = fun x y -> x
50
Arrow as implication
The formula
A ⇒ B ⇒ A
i.e. the type
’a -> ’b -> ’a
can be proved by
let k = fun x y -> x
50
Arrow as implication
The formula
(A ⇒ B) ⇒ (B ⇒ C) ⇒ (A ⇒ C)
i.e. the type
(’a -> ’b) -> (’b -> ’c) -> ’a -> ’c
can be proved by
let comp f g x = g (f x)
51
Arrow as implication
The formula
(A ⇒ B) ⇒ (B ⇒ C) ⇒ (A ⇒ C)
i.e. the type
(’a -> ’b) -> (’b -> ’c) -> ’a -> ’c
can be proved by
let comp f g x = g (f x)
51
Arrow as implication
The formula
(A ⇒ B) ⇒ (B ⇒ C) ⇒ (A ⇒ C)
i.e. the type
(’a -> ’b) -> (’b -> ’c) -> ’a -> ’c
can be proved by
let comp f g x = g (f x)
51
Arrow as implication
The formula
(A ⇒ B) ⇒ (B ⇒ C) ⇒ (A ⇒ C)
i.e. the type
(’a -> ’b) -> (’b -> ’c) -> ’a -> ’c
can be proved by
let comp f g x = g (f x)
51
The proof-as-program correspondence
We will make the following precise:
Theorem
A formula can be proved (for a suitable notion of provability) if and only there is a
program of the corresponding type (for a suitable subset of OCaml).
In other words,
PROGRAM = PROOF
(at least for existence)
52
Conjunction
The correspondence would be boring if it was limited to implication.
The formula
A ∧ B
can be interpreted as the type
’a * ’b
53
Conjunction
The correspondence would be boring if it was limited to implication.
The formula
A ∧ B
can be interpreted as the type
’a * ’b
53
Conjunction
The formula
(A ∧ B) ⇒ A
corresponding to the type
(’a * ’b) -> ’a
can be proved by
let proj1 = fun (x , y) -> x
54
Conjunction
The formula
(A ∧ B) ⇒ A
corresponding to the type
(’a * ’b) -> ’a
can be proved by
let proj1 = fun (x , y) -> x
54
Conjunction
The formula
(A ∧ B) ⇒ A
corresponding to the type
(’a * ’b) -> ’a
can be proved by
let proj1 = fun (x , y) -> x
54
Conjunction
The formula
(A ∧ B) ⇒ A
corresponding to the type
(’a * ’b) -> ’a
can be proved by
let proj1 = fun (x , y) -> x
54
Conjunction
The formula
(A ∧ B) ⇒ (B ∧ A)
corresponding to the type
(’a * ’b) -> (’b * ’a)
can be proved by
let comm = fun (x , y) -> (y , x)
55
Conjunction
The formula
(A ∧ B) ⇒ (B ∧ A)
corresponding to the type
(’a * ’b) -> (’b * ’a)
can be proved by
let comm = fun (x , y) -> (y , x)
55
Conjunction
The formula
(A ∧ B) ⇒ (B ∧ A)
corresponding to the type
(’a * ’b) -> (’b * ’a)
can be proved by
let comm = fun (x , y) -> (y , x)
55
Conjunction
The formula
(A ∧ B) ⇒ (B ∧ A)
corresponding to the type
(’a * ’b) -> (’b * ’a)
can be proved by
let comm = fun (x , y) -> (y , x)
55
Truth
The truth formula
>
can be interpreted as the type
unit
whose only value is
()
56
Truth
The truth formula
>
can be interpreted as the type
unit
whose only value is
()
56
Truth
The formula
A ⇒ >
corresponding to the type
’a -> unit
can be proved by
fun x -> ()
57
Truth
The formula
A ⇒ >
corresponding to the type
’a -> unit
can be proved by
fun x -> ()
57
Truth
The formula
A ⇒ >
corresponding to the type
’a -> unit
can be proved by
fun x -> ()
57
Truth
The formula
A ⇒ >
corresponding to the type
’a -> unit
can be proved by
fun x -> ()
57
Falsity
The falsity formula
⊥
can be interpreted as the type
type empty = |
which is a recursive type with no constructor.
58
Falsity
The falsity formula
⊥
can be interpreted as the type
type empty = |
which is a recursive type with no constructor.
58
Falsity
The formula
⊥ ⇒ A
corresponding to the type
empty -> ’a
can be proved by
let absurd = fun x -> match x with -> .
59
Falsity
The formula
⊥ ⇒ A
corresponding to the type
empty -> ’a
can be proved by
let absurd = fun x -> match x with -> .
59
Falsity
The formula
⊥ ⇒ A
corresponding to the type
empty -> ’a
can be proved by
let absurd = fun x -> match x with -> .
59
Falsity
The formula
⊥ ⇒ A
corresponding to the type
empty -> ’a
can be proved by
let absurd = fun x -> match x with -> .
59
Negation
As usual, negation can be defined as
¬A =
A ⇒ ⊥
which corresponds to the type
’a -> empty
60
Negation
As usual, negation can be defined as
¬A = A ⇒ ⊥
which corresponds to the type
’a -> empty
60
Negation
The contraposition formula
(A ⇒ B) ⇒ (¬B ⇒ ¬A)
corresponding to the type
(’a -> ’b) -> (’b -> empty) -> ’a -> empty
can be proved by
let contr = fun f b’ a -> b’ (f a)
61
Negation
The contraposition formula
(A ⇒ B) ⇒ (¬B ⇒ ¬A)
corresponding to the type
(’a -> ’b) -> (’b -> empty) -> ’a -> empty
can be proved by
let contr = fun f b’ a -> b’ (f a)
61
Negation
The contraposition formula
(A ⇒ B) ⇒ (¬B ⇒ ¬A)
corresponding to the type
(’a -> ’b) -> (’b -> empty) -> ’a -> empty
can be proved by
let contr = fun f b’ a -> b’ (f a)
61
Negation
The contraposition formula
(A ⇒ B) ⇒ (¬B ⇒ ¬A)
corresponding to the type
(’a -> ’b) -> (’b -> empty) -> ’a -> empty
can be proved by
let contr = fun f b’ a -> b’ (f a)
61
Disjunction
The disjunction
A ∨ B
can be interpreted as the recursive type
type ('a , 'b) coprod =
| Left of 'a
| Right of 'b
62
Disjunction
The disjunction
A ∨ B
can be interpreted as the recursive type
type ('a , 'b) coprod =
| Left of 'a
| Right of 'b
62
Disjunction
The distributivity formula
A ∧ (B ∨ C ) ⇒ (A ∧ B) ∨ (A ∧ C )
corresponding to the type
(’a * (’b , ’c) coprod) -> (’a * ’b , ’a * ’c) coprod
can be proved by
let dist = fun (a , x) ->
match x with
| Left b -> Left (a , b)
| Right c -> Right (a , c)
63
Disjunction
The distributivity formula
A ∧ (B ∨ C ) ⇒ (A ∧ B) ∨ (A ∧ C)
corresponding to the type
(’a * (’b , ’c) coprod) -> (’a * ’b , ’a * ’c) coprod
can be proved by
let dist = fun (a , x) ->
match x with
| Left b -> Left (a , b)
| Right c -> Right (a , c)
63
Disjunction
The distributivity formula
A ∧ (B ∨ C ) ⇒ (A ∧ B) ∨ (A ∧ C)
corresponding to the type
(’a * (’b , ’c) coprod) -> (’a * ’b , ’a * ’c) coprod
can be proved by
let dist = fun (a , x) ->
match x with
| Left b -> Left (a , b)
| Right c -> Right (a , c)
63
Disjunction
The distributivity formula
A ∧ (B ∨ C ) ⇒ (A ∧ B) ∨ (A ∧ C)
corresponding to the type
(’a * (’b , ’c) coprod) -> (’a * ’b , ’a * ’c) coprod
can be proved by
let dist = fun (a , x) ->
match x with
| Left b -> Left (a , b)
| Right c -> Right (a , c)
63
Corner cases
The correspondence between
• a formula is provable,
• there exists a program of the corresponding type
is not perfect because
• OCaml is not intended for that, and
• we need to do more theory.
For languages such as Agda, the match is perfect.
64
Corner cases: too many provable formulas
We can prove absurd formulas such as
A ⇒ B
by
• using side effects:
let absurd : 'a -> 'b = fun x -> raise Not_found
• using non-termination:
let rec absurd : 'a -> 'b = fun x -> absurd x
From which we can “prove” pretty much everything:
let fake : empty = absurd ()
65
Corner cases: too many provable formulas
We can prove absurd formulas such as
A ⇒ B
by
• using side effects:
let absurd : 'a -> 'b = fun x -> raise Not_found
• using non-termination:
let rec absurd : 'a -> 'b = fun x -> absurd x
From which we can “prove” pretty much everything:
let fake : empty = absurd ()
65
Corner cases: too many provable formulas
We can prove absurd formulas such as
A ⇒ B
by
• using side effects:
let absurd : 'a -> 'b = fun x -> raise Not_found
• using non-termination:
let rec absurd : 'a -> 'b = fun x -> absurd x
From which we can “prove” pretty much everything:
let fake : empty = absurd ()
65
Corner cases: too many provable formulas
We can prove absurd formulas such as
A ⇒ B
by
• using side effects:
let absurd : 'a -> 'b = fun x -> raise Not_found
• using non-termination:
let rec absurd : 'a -> 'b = fun x -> absurd x
From which we can “prove” pretty much everything:
let fake : empty = absurd ()
65
Corner cases: too few provable formulas
The formula
A ∨ ¬A
corresponding to the type
(’a , ’a -> empty) coprod
has no simple proof.
66
The usefulness of typing
As Milner put it:
Well-typed programs cannot go wrong.
We will see that typed programs are safe:
• subject reduction: typing is preserved along reduction,
• progress: a program which is not a value always reduces,
i.e. execution is never stuck
In order to formalize this, we need to define the reduction and typing of our language.
68
The usefulness of typing
As Milner put it:
Well-typed programs cannot go wrong.
We will see that typed programs are safe:
• subject reduction: typing is preserved along reduction,
• progress: a program which is not a value always reduces,
i.e. execution is never stuck
In order to formalize this, we need to define the reduction and typing of our language.
68
The usefulness of typing
As Milner put it:
Well-typed programs cannot go wrong.
We will see that typed programs are safe:
• subject reduction: typing is preserved along reduction,
• progress: a program which is not a value always reduces,
i.e. execution is never stuck
In order to formalize this, we need to define the reduction and typing of our language.
68
The usefulness of typing
As Milner put it:
Well-typed programs cannot go wrong.
We will see that typed programs are safe:
• subject reduction: typing is preserved along reduction,
• progress: a program which is not a value always reduces,
i.e. execution is never stuck
In order to formalize this, we need to define the reduction and typing of our language.
68
The usefulness of typing
As Milner put it:
Well-typed programs cannot go wrong.
We will see that typed programs are safe:
• subject reduction: typing is preserved along reduction,
• progress: a program which is not a value always reduces,
i.e. execution is never stuck
In order to formalize this, we need to define the reduction and typing of our language.
68
A simple programming language
A program is a term generated by
p, q ::= b a boolean b ∈ {true, false}
| n an integer n ∈ Z
| p + q an addition
| p < q a comparison
| if b then p else q a branching
A value is a program which is either a boolean b or an integer n.
69
A simple programming language
A program is a term generated by
p, q ::= b a boolean b ∈ {true, false}
| n an integer n ∈ Z
| p + q an addition
| p < q a comparison
| if b then p else q a branching
A value is a program which is either a boolean b or an integer n.
69
Typing
A type is either bool or int.
The fact that p has type A is written
` p : A
The typing rules are
` n : int ` b : bool
` p
1
: int ` p
2
: int
` p
1
+ p
2
: int
` p
1
: int ` p
2
: int
` p
1
< p
2
: bool
` p : bool ` p
1
: A ` p
2
: A
` if p then p
1
else p
2
: A
70
Typing
A type is either bool or int.
The fact that p has type A is written
` p : A
The typing rules are
` n : int ` b : bool
` p
1
: int ` p
2
: int
` p
1
+ p
2
: int
` p
1
: int ` p
2
: int
` p
1
< p
2
: bool
` p : bool ` p
1
: A ` p
2
: A
` if p then p
1
else p
2
: A
70
Typing
A type is either bool or int.
The fact that p has type A is written
` p : A
The typing rules are
` n : int ` b : bool
` p
1
: int ` p
2
: int
` p
1
+ p
2
: int
` p
1
: int ` p
2
: int
` p
1
< p
2
: bool
` p : bool ` p
1
: A ` p
2
: A
` if p then p
1
else p
2
: A
70
Typing
A program p has type A when ` p : A can be derived.
For instance:
` 3 : int ` 2 : int
` 3 < 2 : bool ` 5 : int ` 1 : int
` if 3 < 2 then 5 else 1 : int
This is called a derivation tree and we can reason on it.
71
Type uniquenes
Theorem (Uniqueness of typing)
If ` p : A and ` p : B are derivable then A = B.
72
Type uniquenes
Theorem (Uniqueness of typing)
If ` p : A and ` p : B are derivable then A = B.
Proof.
By induction on p (note that there is at most one rule for each form of program):
• if p is of the form p
1
+ p
2
then necessarily the last typing rule is
` p
1
: int ` p
2
: int
` p
1
+ p
2
: int
• . . .
72
Type uniquenes
Theorem (Uniqueness of typing)
If ` p : A and ` p : B are derivable then A = B.
Note: this does not hold in OCaml since
fun x -> x
has types
’a -> ’a int -> int string -> string
but there is a most general one (’a -> ’a), which is the inferred type.
72
Reduction
The reduction relation p −→ q describes when a program p evaluates to q in one step.
It is the smallest relation such that
73
Reduction
The reduction relation p −→ q describes when a program p evaluates to q in one step.
It is the smallest relation such that
n
1
+ n
2
−→ n
1
+ n
2
p
1
−→ p
0
1
p
1
+ p
2
−→ p
0
1
+ p
2
p
2
−→ p
0
2
p
1
+ p
2
−→ p
1
+ p
0
2
For instance:
• 3 + 2 −→ 5
• (6 + 3) + (1 + 1) −→ 9 + (1 + 1)
• (6 + 3) + (1 + 1) −→ (6 + 3) + 2
73
Reduction
The reduction relation p −→ q describes when a program p evaluates to q in one step.
It is the smallest relation such that
n
1
< n
2
n
1
< n
2
−→ true
n
1
> n
2
n
1
< n
2
−→ false
p
1
−→ p
0
1
p
1
< p
2
−→ p
0
1
< p
2
p
2
−→ p
0
2
p
1
< p
2
−→ p
1
< p
0
2
For instance:
(2 + 2) < 3 −→ 4 < 3 −→ false
73
Reduction
The reduction relation p −→ q describes when a program p evaluates to q in one step.
It is the smallest relation such that
if true then p
1
else p
2
−→ p
1
if false then p
1
else p
2
−→ p
2
p −→ p
0
if p then p
1
else p
2
−→ if p
0
then p
1
else p
2
For instance:
if 2 < 3 then 5 + 1 else 9 −→ if true then 5 + 1 else 9
−→ 5 + 1
−→ 6
if 2 < 3 then 5 + 1 else 9 −→ if true then 5 + 1 else 9 −→ 5 + 1 −→ 6
73
Irreducible programs
We have to closely related notions:
• values are either integers or natural numbers,
• irreducible programs are programs that cannot reduce.
Note that values are irreducible:
3 6−→ . . . true 6−→ . . .
but there are irreducible programs which are not values:
• 3 + true
• if 5 then p else q
• . . .
We will prove that for typable programs, the two notions coincide!
74
Irreducible programs
We have to closely related notions:
• values are either integers or natural numbers,
• irreducible programs are programs that cannot reduce.
Note that values are irreducible:
3 6−→ . . . true 6−→ . . .
but there are irreducible programs which are not values:
• 3 + true
• if 5 then p else q
• . . .
We will prove that for typable programs, the two notions coincide!
74
Irreducible programs
We have to closely related notions:
• values are either integers or natural numbers,
• irreducible programs are programs that cannot reduce.
Note that values are irreducible:
3 6−→ . . . true 6−→ . . .
but there are irreducible programs which are not values:
• 3 + true
• if 5 then p else q
• . . .
We will prove that for typable programs, the two notions coincide!
74
Irreducible programs
We have to closely related notions:
• values are either integers or natural numbers,
• irreducible programs are programs that cannot reduce.
Note that values are irreducible:
3 6−→ . . . true 6−→ . . .
but there are irreducible programs which are not values:
• 3 + true
• if 5 then p else q
• . . .
We will prove that for typable programs, the two notions coincide!
74
Irreducible programs
We have to closely related notions:
• values are either integers or natural numbers,
• irreducible programs are programs that cannot reduce.
Note that values are irreducible:
3 6−→ . . . true 6−→ . . .
but there are irreducible programs which are not values:
• 3 + true
• if 5 then p else q
• . . .
We will prove that for typable programs, the two notions coincide!
74
Safety: subject reduction
Theorem (Subject reduction)
If p −→ p
0
and p has type A then p
0
also has type A.
Proof.
By induction on the derivation of p −→ p
0
.
If the last rule is
p
1
−→ p
0
1
p
1
+ p
2
−→ p
0
1
+ p
2
then the derivation of ` p : A
necessarily ends with
` p
1
: int ` p
2
: int
` p
1
+ p
2
: int
thus ` p
1
: int is derivable,
thus ` p
0
1
: int is derivable by induction
hypothesis,
thus ` p
0
1
+ p
2
: int is derivable:
` p
0
1
: int ` p
2
: int
` p
0
1
+ p
2
: int
Other cases are similar.
75
Safety: subject reduction
Theorem (Subject reduction)
If p −→ p
0
and p has type A then p
0
also has type A.
Proof.
By induction on the derivation of p −→ p
0
.
If the last rule is
p
1
−→ p
0
1
p
1
+ p
2
−→ p
0
1
+ p
2
then the derivation of ` p : A
necessarily ends with
` p
1
: int ` p
2
: int
` p
1
+ p
2
: int
thus ` p
1
: int is derivable,
thus ` p
0
1
: int is derivable by induction
hypothesis,
thus ` p
0
1
+ p
2
: int is derivable:
` p
0
1
: int ` p
2
: int
` p
0
1
+ p
2
: int
Other cases are similar.
75
Safety: subject reduction
Theorem (Subject reduction)
If p −→ p
0
and p has type A then p
0
also has type A.
Proof.
By induction on the derivation of p −→ p
0
.
If the last rule is
p
1
−→ p
0
1
p
1
+ p
2
−→ p
0
1
+ p
2
then the derivation of ` p : A
necessarily ends with
` p
1
: int ` p
2
: int
` p
1
+ p
2
: int
thus ` p
1
: int is derivable,
thus ` p
0
1
: int is derivable by induction
hypothesis,
thus ` p
0
1
+ p
2
: int is derivable:
` p
0
1
: int ` p
2
: int
` p
0
1
+ p
2
: int
Other cases are similar.
75
Safety: subject reduction
Theorem (Subject reduction)
If p −→ p
0
and p has type A then p
0
also has type A.
Proof.
By induction on the derivation of p −→ p
0
.
If the last rule is
p
1
−→ p
0
1
p
1
+ p
2
−→ p
0
1
+ p
2
then the derivation of ` p : A
necessarily ends with
` p
1
: int ` p
2
: int
` p
1
+ p
2
: int
thus ` p
1
: int is derivable,
thus ` p
0
1
: int is derivable by induction
hypothesis,
thus ` p
0
1
+ p
2
: int is derivable:
` p
0
1
: int ` p
2
: int
` p
0
1
+ p
2
: int
Other cases are similar.
75
Safety: subject reduction
Theorem (Subject reduction)
If p −→ p
0
and p has type A then p
0
also has type A.
Proof.
By induction on the derivation of p −→ p
0
.
If the last rule is
p
1
−→ p
0
1
p
1
+ p
2
−→ p
0
1
+ p
2
then the derivation of ` p : A
necessarily ends with
` p
1
: int ` p
2
: int
` p
1
+ p
2
: int
thus ` p
1
: int is derivable,
thus ` p
0
1
: int is derivable by induction
hypothesis,
thus ` p
0
1
+ p
2
: int is derivable:
` p
0
1
: int ` p
2
: int
` p
0
1
+ p
2
: int
Other cases are similar.
75
Safety: subject reduction
Theorem (Subject reduction)
If p −→ p
0
and p has type A then p
0
also has type A.
Proof.
By induction on the derivation of p −→ p
0
.
If the last rule is
p
1
−→ p
0
1
p
1
+ p
2
−→ p
0
1
+ p
2
then the derivation of ` p : A
necessarily ends with
` p
1
: int ` p
2
: int
` p
1
+ p
2
: int
thus ` p
1
: int is derivable,
thus ` p
0
1
: int is derivable by induction
hypothesis,
thus ` p
0
1
+ p
2
: int is derivable:
` p
0
1
: int ` p
2
: int
` p
0
1
+ p
2
: int
Other cases are similar.
75
Safety: subject reduction
Theorem (Subject reduction)
If p −→ p
0
and p has type A then p
0
also has type A.
Proof.
By induction on the derivation of p −→ p
0
.
If the last rule is
p
1
−→ p
0
1
p
1
+ p
2
−→ p
0
1
+ p
2
then the derivation of ` p : A
necessarily ends with
` p
1
: int ` p
2
: int
` p
1
+ p
2
: int
thus ` p
1
: int is derivable,
thus ` p
0
1
: int is derivable by induction
hypothesis,
thus ` p
0
1
+ p
2
: int is derivable:
` p
0
1
: int ` p
2
: int
` p
0
1
+ p
2
: int
Other cases are similar.
75
Safety: subject reduction
Theorem (Subject reduction)
If p −→ p
0
and p has type A then p
0
also has type A.
Proof.
By induction on the derivation of p −→ p
0
.
If the last rule is
p
1
−→ p
0
1
p
1
+ p
2
−→ p
0
1
+ p
2
then the derivation of ` p : A
necessarily ends with
` p
1
: int ` p
2
: int
` p
1
+ p
2
: int
thus ` p
1
: int is derivable,
thus ` p
0
1
: int is derivable by induction
hypothesis,
thus ` p
0
1
+ p
2
: int is derivable:
` p
0
1
: int ` p
2
: int
` p
0
1
+ p
2
: int
Other cases are similar.
75
Safety: progress
Theorem (Progress)
If p is a program of type A which is not value then p reduces (to some p
0
).
Proof.
By induction on the derivation of ` p : A.
Suppose that the last rule is
` p
1
: int ` p
2
: int
` p
1
+ p
2
: int
If p
1
is not a value then, by induction
hypothesis, p
1
−→ p
0
1
and thus
p
1
+ p
2
−→ p
0
1
+ p
2
.
If p
2
is not a value then, by induction
hypothesis, p
2
−→ p
0
2
and thus
p
1
+ p
2
−→ p
1
+ p
0
2
.
If both p
1
and p
2
are values then they
necessarily integers and thus
p
1
+ p
2
−→ p
0
1
+ n.
Other cases are similar.
76
Safety: progress
Theorem (Progress)
If p is a program of type A which is not value then p reduces (to some p
0
).
Proof.
By induction on the derivation of ` p : A.
Suppose that the last rule is
` p
1
: int ` p
2
: int
` p
1
+ p
2
: int
If p
1
is not a value then, by induction
hypothesis, p
1
−→ p
0
1
and thus
p
1
+ p
2
−→ p
0
1
+ p
2
.
If p
2
is not a value then, by induction
hypothesis, p
2
−→ p
0
2
and thus
p
1
+ p
2
−→ p
1
+ p
0
2
.
If both p
1
and p
2
are values then they
necessarily integers and thus
p
1
+ p
2
−→ p
0
1
+ n.
Other cases are similar.
76
Safety: progress
Theorem (Progress)
If p is a program of type A which is not value then p reduces (to some p
0
).
Proof.
By induction on the derivation of ` p : A.
Suppose that the last rule is
` p
1
: int ` p
2
: int
` p
1
+ p
2
: int
If p
1
is not a value then, by induction
hypothesis, p
1
−→ p
0
1
and thus
p
1
+ p
2
−→ p
0
1
+ p
2
.
If p
2
is not a value then, by induction
hypothesis, p
2
−→ p
0
2
and thus
p
1
+ p
2
−→ p
1
+ p
0
2
.
If both p
1
and p
2
are values then they
necessarily integers and thus
p
1
+ p
2
−→ p
0
1
+ n.
Other cases are similar.
76
Safety: progress
Theorem (Progress)
If p is a program of type A which is not value then p reduces (to some p
0
).
Proof.
By induction on the derivation of ` p : A.
Suppose that the last rule is
` p
1
: int ` p
2
: int
` p
1
+ p
2
: int
If p
1
is not a value then, by induction
hypothesis, p
1
−→ p
0
1
and thus
p
1
+ p
2
−→ p
0
1
+ p
2
.
If p
2
is not a value then, by induction
hypothesis, p
2
−→ p
0
2
and thus
p
1
+ p
2
−→ p
1
+ p
0
2
.
If both p
1
and p
2
are values then they
necessarily integers and thus
p
1
+ p
2
−→ p
0
1
+ n.
Other cases are similar.
76
Safety: progress
Theorem (Progress)
If p is a program of type A which is not value then p reduces (to some p
0
).
Proof.
By induction on the derivation of ` p : A.
Suppose that the last rule is
` p
1
: int ` p
2
: int
` p
1
+ p
2
: int
If p
1
is not a value then, by induction
hypothesis, p
1
−→ p
0
1
and thus
p
1
+ p
2
−→ p
0
1
+ p
2
.
If p
2
is not a value then, by induction
hypothesis, p
2
−→ p
0
2
and thus
p
1
+ p
2
−→ p
1
+ p
0
2
.
If both p
1
and p
2
are values then they
necessarily integers and thus
p
1
+ p
2
−→ p
0
1
+ n.
Other cases are similar.
76
Safety: progress
Theorem (Progress)
If p is a program of type A which is not value then p reduces (to some p
0
).
Proof.
By induction on the derivation of ` p : A.
Suppose that the last rule is
` p
1
: int ` p
2
: int
` p
1
+ p
2
: int
If p
1
is not a value then, by induction
hypothesis, p
1
−→ p
0
1
and thus
p
1
+ p
2
−→ p
0
1
+ p
2
.
If p
2
is not a value then, by induction
hypothesis, p
2
−→ p
0
2
and thus
p
1
+ p
2
−→ p
1
+ p
0
2
.
If both p
1
and p
2
are values then they
necessarily integers and thus
p
1
+ p
2
−→ p
0
1
+ n.
Other cases are similar.
76
Safety: progress
Theorem (Progress)
If p is a program of type A which is not value then p reduces (to some p
0
).
Proof.
By induction on the derivation of ` p : A.
Suppose that the last rule is
` p
1
: int ` p
2
: int
` p
1
+ p
2
: int
If p
1
is not a value then, by induction
hypothesis, p
1
−→ p
0
1
and thus
p
1
+ p
2
−→ p
0
1
+ p
2
.
If p
2
is not a value then, by induction
hypothesis, p
2
−→ p
0
2
and thus
p
1
+ p
2
−→ p
1
+ p
0
2
.
If both p
1
and p
2
are values then they
necessarily integers and thus
p
1
+ p
2
−→ p
0
1
+ n.
Other cases are similar.
76
Safety
Theorem (Safety)
Given a program p of type A, either
• there is an infinite sequence of reductions: p −→ p
1
−→ p
2
−→ . . .,
• or the reduction ends on a value: p −→ p
1
−→ p
2
−→ . . . −→ p
n
= v .
Proof.
Suppose given a finite sequence of reductions from p,
p −→ p
1
−→ . . . −→ p
n
such that all the p
i
are of type A. Then, by progress, either
• p
n
is a value, or
• p
n
−→ p
n+1
and p
n+1
is of type A by subject reduction.
77
Safety
Theorem (Safety)
Given a program p of type A, either
• there is an infinite sequence of reductions: p −→ p
1
−→ p
2
−→ . . .,
• or the reduction ends on a value: p −→ p
1
−→ p
2
−→ . . . −→ p
n
= v .
Proof.
Suppose given a finite sequence of reductions from p,
p −→ p
1
−→ . . . −→ p
n
such that all the p
i
are of type A. Then, by progress, either
• p
n
is a value, or
• p
n
−→ p
n+1
and p
n+1
is of type A by subject reduction.
77
Safety
The typing system thus ensures that we will never get stuck because we have the
wrong data:
true + 3
We are on the safe side, but we reject legit programs:
if true then 3 else false
We only prevent data errors, but not all errors: the program
let f x = 1 / (x - 2)
should be given the type
{n : int | n 6= 2} -> int
78
Safety
The typing system thus ensures that we will never get stuck because we have the
wrong data:
true + 3
We are on the safe side, but we reject legit programs:
if true then 3 else false
We only prevent data errors, but not all errors: the program
let f x = 1 / (x - 2)
should be given the type
{n : int | n 6= 2} -> int
78
Safety
The typing system thus ensures that we will never get stuck because we have the
wrong data:
true + 3
We are on the safe side, but we reject legit programs:
if true then 3 else false
We only prevent data errors, but not all errors: the program
let f x = 1 / (x - 2)
should be given the type
{n : int | n 6= 2} -> int
78
Recursive definitions
We write U for a set, which we think of as all possible OCaml values.
We write P(U) for the set of subsets of U.
Given F : P(U) → P(U) we say that X ∈ P(U) is a
• prefixpoint when F (X ) ⊆ X ,
• fixpoint when F (X ) = X .
80
Recursive definitions
We write U for a set, which we think of as all possible OCaml values.
We write P(U) for the set of subsets of U.
Given F : P(U) → P(U) we say that X ∈ P(U) is a
• prefixpoint when F (X ) ⊆ X ,
• fixpoint when F (X ) = X .
80
Recursive definitions
Consider the following type for binary trees labeled by integers:
type tree =
| Leaf of int
| Node of int * tree * tree
81
Recursive definitions
Consider the following type for binary trees labeled by integers:
type tree =
| Leaf of int
| Node of int * tree * tree
For instance, we have the tree
3
1
4 3
2
Node (3, Node (1, Leaf 4, Leaf 3), Leaf 2)
81
Recursive definitions
Consider the following type for binary trees labeled by integers:
type tree =
| Leaf of int
| Node of int * tree * tree
For instance, we have the tree
3
1
4 3
2
Node (3, Node (1, Leaf 4, Leaf 3), Leaf 2)
81
Recursive definitions
Consider the following type for binary trees labeled by integers:
type tree =
| Leaf of int
| Node of int * tree * tree
For instance, we have the tree
3
1
4 3
2
Node (3, Node (1, Leaf 4, Leaf 3), Leaf 2)
81
Recursive definitions
Consider the following type for binary trees labeled by integers:
type tree =
| Leaf of int
| Node of int * tree * tree
This type induces a function F : P(U) → P(U) defined by
F (X ) = {Node(n,t
1
,t
2
) | n ∈ N and t
1
, t
2
∈ X } ∪ {Leaf(n) | n ∈ N}
and the set T of trees is the smallest subset of U such that
F (T ) ⊆ T
It turns out that we actually have F (T ) = T and it is the smallest such.
81
Recursive definitions
Consider the following type for binary trees labeled by integers:
type tree =
| Leaf of int
| Node of int * tree * tree
This type induces a function F : P(U) → P(U) defined by
F (X ) = {Node(n,t
1
,t
2
) | n ∈ N and t
1
, t
2
∈ X } ∪ {Leaf(n) | n ∈ N}
and the set T of trees is the smallest subset of U such that
F (T ) ⊆ T
It turns out that we actually have F (T ) = T and it is the smallest such.
81
Recursive definitions
Consider the following type for binary trees labeled by integers:
type tree =
| Leaf of int
| Node of int * tree * tree
This type induces a function F : P(U) → P(U) defined by
F (X ) = {Node(n,t
1
,t
2
) | n ∈ N and t
1
, t
2
∈ X } ∪ {Leaf(n) | n ∈ N}
and the set T of trees is the smallest subset of U such that
F (T ) ⊆ T
It turns out that we actually have F (T ) = T and it is the smallest such.
81
Recursive definitions
First note that the function
F (X ) = {Node(n,t
1
,t
2
) | n ∈ N and t
1
, t
2
∈ X } ∪ {Leaf(n) | n ∈ N}
is increasing:
X ⊆ Y implies F (X ) ⊆ F (Y )
We will see that for such a function
• the smallest prefixpoint exists, and
• it coincides with the smallest fixpoint.
82
Recursive definitions
First note that the function
F (X ) = {Node(n,t
1
,t
2
) | n ∈ N and t
1
, t
2
∈ X } ∪ {Leaf(n) | n ∈ N}
is increasing:
X ⊆ Y implies F (X ) ⊆ F (Y )
We will see that for such a function
• the smallest prefixpoint exists, and
• it coincides with the smallest fixpoint.
82
The Knaster-Tarski theorem
Theorem
Given an increasing F : P(U) → P(U), the set
fix(F ) =
\
{X ∈ P(U) | F (X ) ⊆ X }
is the least fixpoint of F :
• we have F (fix(F )) = fix(F )
• and fix(F ) ⊆ X for every fixpoint X of F .
83
The Knaster-Tarski theorem: proof
Proof.
We write C = {X ∈ P(U) | F (X ) ⊆ X }.
Given X ∈ C, we have fix(F ) =
T
C ⊆ X (*)
and therefore, since F is increasing, F (fix(F )) ⊆ F (X ) ⊆ X (**)
from which we deduce F (fix(F )) ⊆
T
C = fix(F).
Moreover, by monotonicity again, we have F (F (fix(F ))) ⊆ F (fix(F ))
therefore, F (fix(F )) ∈ C,
and thus, by (*), fix(F ) ⊆ F (fix(F ))
We have shown that fix(F ) is a fixpoint of F .
Given a fixpoint X of F , we have X ∈ C
thus, by (**), fix(F ) = F (fix(F )) ⊆ X
i.e. fix(F ) is the smallest fixpoint.
84
The Knaster-Tarski theorem: proof
Proof.
We write C = {X ∈ P(U) | F (X ) ⊆ X }.
Given X ∈ C, we have fix(F ) =
T
C ⊆ X (*)
and therefore, since F is increasing, F (fix(F )) ⊆ F (X ) ⊆ X (**)
from which we deduce F (fix(F )) ⊆
T
C = fix(F).
Moreover, by monotonicity again, we have F (F (fix(F ))) ⊆ F (fix(F ))
therefore, F (fix(F )) ∈ C,
and thus, by (*), fix(F ) ⊆ F (fix(F ))
We have shown that fix(F ) is a fixpoint of F .
Given a fixpoint X of F , we have X ∈ C
thus, by (**), fix(F ) = F (fix(F )) ⊆ X
i.e. fix(F ) is the smallest fixpoint.
84
The Knaster-Tarski theorem: proof
Proof.
We write C = {X ∈ P(U) | F (X ) ⊆ X }.
Given X ∈ C, we have fix(F ) =
T
C ⊆ X (*)
and therefore, since F is increasing, F (fix(F )) ⊆ F (X ) ⊆ X (**)
from which we deduce F (fix(F )) ⊆
T
C = fix(F).
Moreover, by monotonicity again, we have F (F (fix(F ))) ⊆ F (fix(F ))
therefore, F (fix(F )) ∈ C,
and thus, by (*), fix(F ) ⊆ F (fix(F ))
We have shown that fix(F ) is a fixpoint of F .
Given a fixpoint X of F , we have X ∈ C
thus, by (**), fix(F ) = F (fix(F )) ⊆ X
i.e. fix(F ) is the smallest fixpoint.
84
The Knaster-Tarski theorem: proof
Proof.
We write C = {X ∈ P(U) | F (X ) ⊆ X }.
Given X ∈ C, we have fix(F ) =
T
C ⊆ X (*)
and therefore, since F is increasing, F (fix(F )) ⊆ F (X ) ⊆ X (**)
from which we deduce F (fix(F )) ⊆
T
C = fix(F).
Moreover, by monotonicity again, we have F (F (fix(F ))) ⊆ F (fix(F ))
therefore, F (fix(F )) ∈ C,
and thus, by (*), fix(F ) ⊆ F (fix(F ))
We have shown that fix(F ) is a fixpoint of F .
Given a fixpoint X of F , we have X ∈ C
thus, by (**), fix(F ) = F (fix(F )) ⊆ X
i.e. fix(F ) is the smallest fixpoint.
84
The Knaster-Tarski theorem: proof
Proof.
We write C = {X ∈ P(U) | F (X ) ⊆ X }.
Given X ∈ C, we have fix(F ) =
T
C ⊆ X (*)
and therefore, since F is increasing, F (fix(F )) ⊆ F (X ) ⊆ X (**)
from which we deduce F (fix(F )) ⊆
T
C = fix(F).
Moreover, by monotonicity again, we have F (F (fix(F ))) ⊆ F (fix(F ))
therefore, F (fix(F )) ∈ C,
and thus, by (*), fix(F ) ⊆ F (fix(F ))
We have shown that fix(F ) is a fixpoint of F .
Given a fixpoint X of F , we have X ∈ C
thus, by (**), fix(F ) = F (fix(F )) ⊆ X
i.e. fix(F ) is the smallest fixpoint.
84
The Knaster-Tarski theorem: proof
Proof.
We write C = {X ∈ P(U) | F (X ) ⊆ X }.
Given X ∈ C, we have fix(F ) =
T
C ⊆ X (*)
and therefore, since F is increasing, F (fix(F )) ⊆ F (X ) ⊆ X (**)
from which we deduce F (fix(F )) ⊆
T
C = fix(F).
Moreover, by monotonicity again, we have F (F (fix(F ))) ⊆ F (fix(F ))
therefore, F (fix(F )) ∈ C,
and thus, by (*), fix(F ) ⊆ F (fix(F ))
We have shown that fix(F ) is a fixpoint of F .
Given a fixpoint X of F , we have X ∈ C
thus, by (**), fix(F ) = F (fix(F )) ⊆ X
i.e. fix(F ) is the smallest fixpoint.
84
The Knaster-Tarski theorem: proof
Proof.
We write C = {X ∈ P(U) | F (X ) ⊆ X }.
Given X ∈ C, we have fix(F ) =
T
C ⊆ X (*)
and therefore, since F is increasing, F (fix(F )) ⊆ F (X ) ⊆ X (**)
from which we deduce F (fix(F )) ⊆
T
C = fix(F).
Moreover, by monotonicity again, we have F (F (fix(F ))) ⊆ F (fix(F ))
therefore, F (fix(F )) ∈ C,
and thus, by (*), fix(F ) ⊆ F (fix(F ))
We have shown that fix(F ) is a fixpoint of F .
Given a fixpoint X of F , we have X ∈ C
thus, by (**), fix(F ) = F (fix(F )) ⊆ X
i.e. fix(F ) is the smallest fixpoint.
84
The Knaster-Tarski theorem: proof
Proof.
We write C = {X ∈ P(U) | F (X ) ⊆ X }.
Given X ∈ C, we have fix(F ) =
T
C ⊆ X (*)
and therefore, since F is increasing, F (fix(F )) ⊆ F (X ) ⊆ X (**)
from which we deduce F (fix(F )) ⊆
T
C = fix(F).
Moreover, by monotonicity again, we have F (F (fix(F ))) ⊆ F (fix(F ))
therefore, F (fix(F )) ∈ C,
and thus, by (*), fix(F ) ⊆ F (fix(F ))
We have shown that fix(F ) is a fixpoint of F .
Given a fixpoint X of F , we have X ∈ C
thus, by (**), fix(F ) = F (fix(F )) ⊆ X
i.e. fix(F ) is the smallest fixpoint.
84
The Knaster-Tarski theorem: proof
Proof.
We write C = {X ∈ P(U) | F (X ) ⊆ X }.
Given X ∈ C, we have fix(F ) =
T
C ⊆ X (*)
and therefore, since F is increasing, F (fix(F )) ⊆ F (X ) ⊆ X (**)
from which we deduce F (fix(F )) ⊆
T
C = fix(F).
Moreover, by monotonicity again, we have F (F (fix(F ))) ⊆ F (fix(F ))
therefore, F (fix(F )) ∈ C,
and thus, by (*), fix(F ) ⊆ F (fix(F ))
We have shown that fix(F ) is a fixpoint of F .
Given a fixpoint X of F , we have X ∈ C
thus, by (**), fix(F ) = F (fix(F )) ⊆ X
i.e. fix(F ) is the smallest fixpoint.
84
The Knaster-Tarski theorem: proof
Proof.
We write C = {X ∈ P(U) | F (X ) ⊆ X }.
Given X ∈ C, we have fix(F ) =
T
C ⊆ X (*)
and therefore, since F is increasing, F (fix(F )) ⊆ F (X ) ⊆ X (**)
from which we deduce F (fix(F )) ⊆
T
C = fix(F).
Moreover, by monotonicity again, we have F (F (fix(F ))) ⊆ F (fix(F ))
therefore, F (fix(F )) ∈ C,
and thus, by (*), fix(F ) ⊆ F (fix(F ))
We have shown that fix(F ) is a fixpoint of F .
Given a fixpoint X of F , we have X ∈ C
thus, by (**), fix(F ) = F (fix(F )) ⊆ X
i.e. fix(F ) is the smallest fixpoint.
84
The Knaster-Tarski theorem: proof
Proof.
We write C = {X ∈ P(U) | F (X ) ⊆ X }.
Given X ∈ C, we have fix(F ) =
T
C ⊆ X (*)
and therefore, since F is increasing, F (fix(F )) ⊆ F (X ) ⊆ X (**)
from which we deduce F (fix(F )) ⊆
T
C = fix(F).
Moreover, by monotonicity again, we have F (F (fix(F ))) ⊆ F (fix(F ))
therefore, F (fix(F )) ∈ C,
and thus, by (*), fix(F ) ⊆ F (fix(F ))
We have shown that fix(F ) is a fixpoint of F .
Given a fixpoint X of F , we have X ∈ C
thus, by (**), fix(F ) = F (fix(F )) ⊆ X
i.e. fix(F ) is the smallest fixpoint.
84
Recursive definitions
Given a recursive type inducing a function F , we can think of fix(F ) as its set of
elements.
85
The Knaster-Tarski theorem
Note that the Knaster-Tarski theorem generalizes to any complete semilattice.
86
The Kleene fixpoint theorem
Under the more subtle hypothesis of the Kleene fixpoint theorem (P(U) is a directed
complete partial order and F is Scott-continuous), one can even show that
fix(F ) =
[
n∈N
F
n
(∅)
i.e. the fixpoint can be obtained by iterating F from the empty set. In the case of
trees,
F
0
(∅) = ∅
F
1
(∅) = {Leaf(n) | n ∈ N}
F
2
(∅) = {Leaf(n) | n ∈ N} ∪ {Nodes(n,t
1
,t
2
) | n ∈ N and t
1
, t
2
∈ F
1
(∅)}
and more generally, F
n
(∅) is the set of trees of height strictly below n. The theorem
states that any tree is a tree of some (finite) height.
87
Induction on recursive types
As a direct corollary,
Theorem (Induction principle)
Given a set X such that F (X ) ⊆ X , we have fix(F ) ⊆ X .
This is abstractly an induction principle on types.
88
Induction on recursive types
Consider the type of natural numbers
type nat = Zero | Suc of nat
Its associated function is
F (X ) = {Zero} ∪ {Suc(n) | n ∈ X }
and its smallest fixpoint is
fix(F ) = {Suc
n
(Zero) | n ∈ N} = {Zero, Suc(Zero), Suc(Suc(Zero)), . . .}
Given a property P(n), consider the set X = {n ∈ N | P(n)}.
We have F (X ) ⊆ X if and only if P(0), and P(n) implies P(S n).
The induction principle, is thus the usual recurrence principle:
P(0) ⇒ (∀n ∈ N.P(n) ⇒ P(S n )) ⇒ (∀n ∈ N.P(n))
89
Induction on recursive types
Consider the type of natural numbers
type nat = Zero | Suc of nat
Its associated function is
F (X ) = {Zero} ∪ {Suc(n) | n ∈ X }
and its smallest fixpoint is
fix(F ) = {Suc
n
(Zero) | n ∈ N} = {Zero, Suc(Zero), Suc(Suc(Zero)), . . .}
Given a property P(n), consider the set X = {n ∈ N | P(n)}.
We have F (X ) ⊆ X if and only if P(0), and P(n) implies P(S n).
The induction principle, is thus the usual recurrence principle:
P(0) ⇒ (∀n ∈ N.P(n) ⇒ P(S n )) ⇒ (∀n ∈ N.P(n))
89
Induction on recursive types
Consider the type of natural numbers
type nat = Zero | Suc of nat
Its associated function is
F (X ) = {Zero} ∪ {Suc(n) | n ∈ X }
and its smallest fixpoint is
fix(F ) = {Suc
n
(Zero) | n ∈ N} = {Zero, Suc(Zero), Suc(Suc(Zero)), . . .}
Given a property P(n), consider the set X = {n ∈ N | P(n)}.
We have F (X ) ⊆ X if and only if P(0), and P(n) implies P(S n).
The induction principle, is thus the usual recurrence principle:
P(0) ⇒ (∀n ∈ N.P(n) ⇒ P(S n )) ⇒ (∀n ∈ N.P(n))
89
Induction on recursive types
Consider the type of natural numbers
type nat = Zero | Suc of nat
Its associated function is
F (X ) = {Zero} ∪ {Suc(n) | n ∈ X }
and its smallest fixpoint is
fix(F ) = {Suc
n
(Zero) | n ∈ N} = {Zero, Suc(Zero), Suc(Suc(Zero)), . . .}
Given a property P(n), consider the set X = {n ∈ N | P(n)}.
We have F (X ) ⊆ X if and only if P(0), and P(n) implies P(S n).
The induction principle, is thus the usual recurrence principle:
P(0) ⇒ (∀n ∈ N.P(n) ⇒ P(S n )) ⇒ (∀n ∈ N.P(n))
89
Induction on recursive types
Consider the type of natural numbers
type nat = Zero | Suc of nat
Its associated function is
F (X ) = {Zero} ∪ {Suc(n) | n ∈ X }
and its smallest fixpoint is
fix(F ) = {Suc
n
(Zero) | n ∈ N} = {Zero, Suc(Zero), Suc(Suc(Zero)), . . .}
Given a property P(n), consider the set X = {n ∈ N | P(n)}.
We have F (X ) ⊆ X if and only if P(0), and P(n) implies P(S n).
The induction principle, is thus the usual recurrence principle:
P(0) ⇒ (∀n ∈ N.P(n) ⇒ P(S n )) ⇒ (∀n ∈ N.P(n))
89
Induction on recursive types
Consider the type of natural numbers
type nat = Zero | Suc of nat
Its associated function is
F (X ) = {Zero} ∪ {Suc(n) | n ∈ X }
and its smallest fixpoint is
fix(F ) = {Suc
n
(Zero) | n ∈ N} = {Zero, Suc(Zero), Suc(Suc(Zero)), . . .}
Given a property P(n), consider the set X = {n ∈ N | P(n)}.
We have F (X ) ⊆ X if and only if P(0), and P(n) implies P(S n).
The induction principle, is thus the usual recurrence principle:
P(0) ⇒ (∀n ∈ N.P(n) ⇒ P(S n )) ⇒ (∀n ∈ N.P(n))
89
Induction on recursive types
Consider the type empty. We have F (X ) = ∅ and thus fix(F ) = ∅. The induction
principle states
∀x ∈ ∅.P(x)
90
An example of a non-smallest fixpoint
Note that the function
F (X ) = {Zero} ∪ {Suc(n) | n ∈ X }
admits a non-smallest fixpoint:
N t {∞}
91
